e@i.P(e) == e:es-E(es). ((loc(e) = i)  P(e)) 

latex

---

clarification:

existse-at(es; i; e.P(e)) == e:es-E(es). ((es-loc(es; e) = i  Id)  P(e)) 

latex

Definitions	x:A. B(x), es-E(es), P  Q, s = t, Id, loc(e)
FDL editor aliases	existse-at